A:MsgA, i:Id.
AtomFree(ds(A))
 AtomFree(da(A))
 AtomFree(Type;{m:(l:IdLnkt:IdA.dout(l,t))| source(mlnk(m)) = i }) 

latex

Definitions

MsgA, t  T, x:A. B(x), ds(M), IdDeq, AtomFree(d), da(M), KindDeq, Knd, f(a), x.A(x), nat-deq-aux, <a,b>, NatDeq, atom-deq-aux, AtomDeq, #$n, a<b, Void, False, x:AB(x), P  Q, A, AB, , {x:A| B(x) }, , Atom, prod-deq(A;B;a;b), proddeq(a;b), product-deq(A;B;a;b), IdLnkDeq, sum-deq(A;B;a;b), sumdeq(a;b), union-deq(A;B;a;b), M.dout(l,tg), Id, x:AB(x), IdLnk, Type, AtomFree(T;x), s ~ t, s = t, mlnk(m), source(l), Prop, x. t(x), A/x,y. B(x;y), 1of(t)

Lemmas

atom-free-settype, lsrc wf, atom-free-ma-dout, IdLnk wf, atom-free-IdLnk, atom-free-Id, ma-dout wf, Knd wf, Kind-deq wf, ma da wf, atom-free-decl wf, id-deq wf, ma ds wf, Id wf, msga wf